Commentary by Chris Pressey
===========================

<!--
Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.

SPDX-License-Identifier: CC-BY-ND-4.0
-->

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
exception: the ratings may be freely used for any purpose with no limitations.

Unification
---------------

### Unification: A Multidisciplinary Survey

*   rating: 1

Gives a pretty good historical overview.

Has a simple example of resolution.

Has a basic example of parsing with unification-based grammar.

Says some things about unification modulo equational theories.
Under commutivity, there can be more than one MGU, but at most
there will be a finite number.  Under associativity, though,
there can be an infinite number.  Under associativity AND
idempotency, no complete set of GUs exists; for every two
unifiable terms s and t, for every unifier u, there exists
a more general unifier v.

I'm not really sure how it is that you can obtain more and more
GUs without bound, but OK!

### Correcting a Widespread Error in Unification Algorithms

*   rating: 1

Basically it seems easy to forget to remember that unification is symmetric;
if we are unifying some variable X on the LHS with something on the RHS, we do that;
but if we are unifying something (non-variable) on the LHS, we forget to check if
the thing on the RHS is a variable, and unify with it.

Imperative implementations don't have the problem as much, probably because
when destructively updating the thing, it's more obvious if you haven't covered
all cases in testing.

When this error is in unification used in backward chaining (Prolog) it's rare
for it to show up, which is probably why it's so widespread.

Norvig gives some good test cases for any implementation of unification, in particular:

    unify(
      p(X, Y, a),
      p(Y, X, X)
    )

which does have a valid unification (X = Y = a) but causes either a failure or a
hang (depending on occurs check or not) on implementations with the error.

### Notes: Unification

*   rating: 1

.

### mrocklin/unification

*   rating: 1

.

### parsonsmatt/unification: implementation of the first order logic unification algorithm in Haskell

*   rating: 1

.

### jozefg/higher-order-unification: A small implementation of higher-order unification

*   rating: 1

The `explanation.md` file in there has a very good explanation of what's going on.  What is
remarkable to me is that Huet's higher-order unification algorithm is not guaranteed to terminate.
It's basically trying to complete two incomplete programs so that they evaluate to the same
value, which "of course" is an undecidable problem.  So the algorithm is only a semi-decision
procedure.  But in practice it does very well at terminating in the cases that are of interest.